00100	GIVEAX(DISTINCT1,(∀ X)(∀ U)
00150		(DISTINCT U ∧ ¬LMEM(X,U) ≡ DISTINCT CONS(X,U)));
00200	
00300	GIVEAX(DISTINCT2,DISTINCT NIL);
00350	
00400	
00500	GIVEAX(NIL1,NIL='NIL);
00600	
00700	GIVEAX(NIL2,(∀ X)(¬LMEM(X,NIL)));
00800	
00900	GIVEAX(CONS1,(∀ X)(∀ Y)(X=CAR CONS(X,Y))));
01000	
01100	GIVEAX(CONS2,(∀ X) (∀ Y)(Y=CDR CONS(X,Y))));
01200	
01300	GIVEAX(CONS3,(∀ X)(∀ Y)(NIL≠CONS(X,Y)));
     

01400	END;